strong-subtype(A;B) == A  B & {b:B| a:A. b = a }  A & (a1, a2:A. a1 = a2  a1 = a2) 

latex

---

clarification:

strong-subtype(A;B)
== A  B & {b:B| a:A. b = a  B }  A & (a1:A, a2:A. a1 = a2  B  a1 = a2  A) 

latex

Definitions	P  Q, x:A. B(x), x:A. B(x), A & B, strong-subtype(A;B)
FDL editor aliases	strong-subtype